Inference at * 
Iof proof for Lemma assert of bimplies:


  p,q:. ((p  q))  ((p)  (q)) 

latex

 by ((((((RepeatMFor 2 (D 0)) 
CollapseTHENM (BoolEval))) 
CollapseTHENM (AbReduce 0))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 

latex

C1: 

C1: 1. True  False
C1:   False
C.

Definitions	, P  Q, P  Q, True, t  T, tt, ff, if b then t else f fi , b, p q, P  Q, p  q, b, P  Q, x:A. B(x), False, Unit, ,
Lemmas	bool wf, false wf, true wf